Problem:
 g(0(),f(x,x)) -> x
 g(x,s(y)) -> g(f(x,y),0())
 g(s(x),y) -> g(f(x,y),0())
 g(f(x,y),0()) -> f(g(x,0()),g(y,0()))

Proof:
 Complexity Transformation Processor:
  strict:
   g(0(),f(x,x)) -> x
   g(x,s(y)) -> g(f(x,y),0())
   g(s(x),y) -> g(f(x,y),0())
   g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [s](x0) = x0,
     
     [g](x0, x1) = x0 + x1,
     
     [f](x0, x1) = x0 + x1 + 225,
     
     [0] = 40
    orientation:
     g(0(),f(x,x)) = 2x + 265 >= x = x
     
     g(x,s(y)) = x + y >= x + y + 265 = g(f(x,y),0())
     
     g(s(x),y) = x + y >= x + y + 265 = g(f(x,y),0())
     
     g(f(x,y),0()) = x + y + 265 >= x + y + 305 = f(g(x,0()),g(y,0()))
    problem:
     strict:
      g(x,s(y)) -> g(f(x,y),0())
      g(s(x),y) -> g(f(x,y),0())
      g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
     weak:
      g(0(),f(x,x)) -> x
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [s](x0) = x0 + 2,
       
       [g](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + x1,
       
       [0] = 0
      orientation:
       g(x,s(y)) = x + y + 2 >= x + y = g(f(x,y),0())
       
       g(s(x),y) = x + y + 2 >= x + y = g(f(x,y),0())
       
       g(f(x,y),0()) = x + y >= x + y = f(g(x,0()),g(y,0()))
       
       g(0(),f(x,x)) = 2x >= x = x
      problem:
       strict:
        g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
       weak:
        g(x,s(y)) -> g(f(x,y),0())
        g(s(x),y) -> g(f(x,y),0())
        g(0(),f(x,x)) -> x
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 3]
        [0 1]
        interpretation:
                   [1 3]     [6]
         [s](x0) = [0 1]x0 + [4],
         
                       [1 1]     [1 1]     [2]
         [g](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
         
                                 [3]
         [f](x0, x1) = x0 + x1 + [4],
         
               [1]
         [0] = [0]
        orientation:
                         [1 1]    [1 1]    [10]    [1 1]    [1 1]    [9]                       
         g(f(x,y),0()) = [0 1]x + [0 1]y + [4 ] >= [0 1]x + [0 1]y + [4] = f(g(x,0()),g(y,0()))
         
                     [1 1]    [1 4]    [12]    [1 1]    [1 1]    [10]                
         g(x,s(y)) = [0 1]x + [0 1]y + [4 ] >= [0 1]x + [0 1]y + [4 ] = g(f(x,y),0())
         
                     [1 4]    [1 1]    [12]    [1 1]    [1 1]    [10]                
         g(s(x),y) = [0 1]x + [0 1]y + [4 ] >= [0 1]x + [0 1]y + [4 ] = g(f(x,y),0())
         
                         [2 2]    [10]         
         g(0(),f(x,x)) = [0 2]x + [4 ] >= x = x
        problem:
         strict:
          
         weak:
          g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
          g(x,s(y)) -> g(f(x,y),0())
          g(s(x),y) -> g(f(x,y),0())
          g(0(),f(x,x)) -> x
        Qed